$\forall$$A$, $B$:Type, $L_{1}$, $L_{2}$:(($A$$\rightarrow$($B$ + Top)) List).
\\[0ex]p{-}first($L_{1}$ @ $L_{2}$) = p{-}first([p{-}first($L_{1}$); p{-}first($L_{2}$)]) $\in$ $A$$\rightarrow$($B$ + Top)